f(true, x, y) → f(gt(x, y), s(x), s(s(y)))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
↳ QTRS
↳ DependencyPairsProof
f(true, x, y) → f(gt(x, y), s(x), s(s(y)))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
GT(s(u), s(v)) → GT(u, v)
F(true, x, y) → F(gt(x, y), s(x), s(s(y)))
F(true, x, y) → GT(x, y)
f(true, x, y) → f(gt(x, y), s(x), s(s(y)))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
GT(s(u), s(v)) → GT(u, v)
F(true, x, y) → F(gt(x, y), s(x), s(s(y)))
F(true, x, y) → GT(x, y)
f(true, x, y) → f(gt(x, y), s(x), s(s(y)))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
GT(s(u), s(v)) → GT(u, v)
f(true, x, y) → f(gt(x, y), s(x), s(s(y)))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
GT(s(u), s(v)) → GT(u, v)
The value of delta used in the strict ordering is 85/16.
POL(s(x1)) = 5/4 + (15/4)x_1
POL(GT(x1, x2)) = x_1 + (13/4)x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
f(true, x, y) → f(gt(x, y), s(x), s(s(y)))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
F(true, x, y) → F(gt(x, y), s(x), s(s(y)))
f(true, x, y) → f(gt(x, y), s(x), s(s(y)))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)